
(set-logic BV)

(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))

(synth-fun f ( (x (BitVec 64))) (BitVec 64)
(

(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
                    (shl1 Start)
 		    (shr1 Start)
		    (shr4 Start)
		    (shr16 Start)
		    (bvand Start Start)
		    (bvor Start Start)
		    (bvxor Start Start)
		    (bvadd Start Start)
		    (if0 Start Start Start)
 ))
)
)


(constraint (= (f #xeb3948e80834a7b8) #xeb3948e80834a7b9))
(constraint (= (f #xc5e6dc51ade49dd6) #xc5e6dc51ade49dd7))
(constraint (= (f #xa95183e445d90dec) #xa95183e445d90dec))
(constraint (= (f #x1be350e7da6e10c0) #x1be350e7da6e10c0))
(constraint (= (f #xbee1574d67553190) #xbee1574d67553191))
(constraint (= (f #x74cee69c4c6c844c) #x74cee69c4c6c844c))
(constraint (= (f #x2a1717252e917032) #x2a1717252e917033))
(constraint (= (f #x2932c0c14e84bec2) #x2932c0c14e84bec2))
(constraint (= (f #x187ec8525edaab1b) #x1942be94f1d18073))
(constraint (= (f #xcd94d63e60eb5d3a) #xcd94d63e60eb5d3b))
(constraint (= (f #x8d232679a758401b) #x918c3fad7493021b))
(constraint (= (f #xb60ba9b5263e8c01) #xbbbc0702cf708061))
(constraint (= (f #x6541c9d20d450ab5) #x686bd8209daf330a))
(constraint (= (f #x15283e46e69400c6) #x15283e46e69400c6))
(constraint (= (f #xab13aea161180eb3) #xb06c4c166c20cf28))
(constraint (= (f #x2d63eb53b6b04eeb) #x2ecf0aae5465d162))
(constraint (= (f #x608e7e4602b04d06) #x608e7e4602b04d06))
(constraint (= (f #xde8619c607731ee6) #xde8619c607731ee6))
(constraint (= (f #xa9be4a508d987ed0) #xa9be4a508d987ed1))
(constraint (= (f #x4e5bc5c16e94abe5) #x50cea3ef7a095144))
(constraint (= (f #x60a8e38829360eb9) #x63ae2aa46a7fbf2e))
(constraint (= (f #x7aae0b19b9c330e1) #x7e837b7287914a68))
(constraint (= (f #x79120dc0558e6ea3) #x7cda9e2e583ae218))
(constraint (= (f #xbceed865e9c99b06) #xbceed865e9c99b06))
(constraint (= (f #x3932672215e4b330) #x3932672215e4b331))
(constraint (= (f #xd47120eee6188248) #xd47120eee6188248))
(constraint (= (f #xebca5aa47248e54e) #xebca5aa47248e54e))
(constraint (= (f #xb53ae157d88a1e13) #xbae4b862974e6f03))
(constraint (= (f #x13db6d3a1173e7de) #x13db6d3a1173e7df))
(constraint (= (f #xba26e8129315b85b) #xbff81f5327ae661d))
(constraint (= (f #x53be5ee8c708c562) #x53be5ee8c708c562))
(constraint (= (f #x5299b8102be85541) #x552e85d0ad4797eb))
(constraint (= (f #xe1728d9be553d8ee) #xe1728d9be553d8ee))
(constraint (= (f #x69d678a4ee60be9a) #x69d678a4ee60be9b))
(constraint (= (f #xca7b51e7ca0e1a0e) #xca7b51e7ca0e1a0e))
(constraint (= (f #x75e52aa094bd9544) #x75e52aa094bd9544))
(constraint (= (f #x8361eedda7d6dc33) #x877cfe5495159314))
(constraint (= (f #xde5841eb2e0eb77e) #xde5841eb2e0eb77f))
(constraint (= (f #x018c259e7e9dab15) #x019886cb7292986d))
(constraint (= (f #xad0eecd8b558eee9) #xb277643f7b03b660))
(constraint (= (f #xb3c3b29dc5be9ead) #xb961d032b3ec93a2))
(constraint (= (f #xe809945e64682d2b) #xef49e101578b6e94))
(constraint (= (f #xc841ee7e66d1b4ca) #xc841ee7e66d1b4ca))
(constraint (= (f #x8234de344e2ee554) #x8234de344e2ee555))
(constraint (= (f #x3ec691ebc0424944) #x3ec691ebc0424944))
(constraint (= (f #x477b794139c7b523) #x49b7550b4395f2cc))
(constraint (= (f #x9ec3a0e7d35de7e8) #x9ec3a0e7d35de7e8))
(constraint (= (f #x11d0a2dd19ec435e) #x11d0a2dd19ec435f))
(constraint (= (f #x0454eb1d04d953dd) #x04779275ed001e7b))
(constraint (= (f #x72631eab187bd32c) #x72631eab187bd32c))
(constraint (= (f #xadc387ee34611d0e) #xadc387ee34611d0e))
(constraint (= (f #x60b6309edeb7567e) #x60b6309edeb7567f))
(constraint (= (f #xb94ae574c60d0e48) #xb94ae574c60d0e48))
(constraint (= (f #xab15904035ee232a) #xab15904035ee232a))
(constraint (= (f #xd53eb736ed729abe) #xd53eb736ed729abf))
(constraint (= (f #x0269b2a7ec918ce4) #x0269b2a7ec918ce4))
(constraint (= (f #x3ea02dd28263cc72) #x3ea02dd28263cc73))
(constraint (= (f #xb96a054bae0aa70a) #xb96a054bae0aa70a))
(constraint (= (f #xbb2e1c5b4cad0876) #xbb2e1c5b4cad0877))
(constraint (= (f #xa691603d40794379) #xabc5eb3f2a7d0d94))
(constraint (= (f #xc7a5e5be8c024e67) #xcde314ec806260da))
(constraint (= (f #x45c7d808c3d4b482) #x45c7d808c3d4b482))
(constraint (= (f #xae590331d9b1aad1) #xb3cbcb4b687f3827))
(constraint (= (f #xec10c0a4a599e10a) #xec10c0a4a599e10a))
(constraint (= (f #x4ac658aeec91de01) #x4d1c8b7463f66cf1))
(constraint (= (f #x3b93cea97e0466d1) #x3d706d1ec9f48a07))
(constraint (= (f #x4b2d629362e61e97) #x4d86cda7fdfd4f8b))
(constraint (= (f #x7c2562e3e73817de) #x7c2562e3e73817df))
(constraint (= (f #xce8793eb6c0434b1) #xd4fbd08ac7645656))
(constraint (= (f #x429cb8d2916eee7e) #x429cb8d2916eee7f))
(constraint (= (f #xda71e769724e427b) #xe14576a4bde0b48e))
(constraint (= (f #x7ba3522b3022e88d) #x7f806cbc89a3ffd1))
(constraint (= (f #x29480c29da2dce27) #x2a924c8b28ff3c98))
(constraint (= (f #x8085c7684e4c0c9d) #x8489f5a390be6d01))
(constraint (= (f #x2cbd597d85677787) #x2e2344497192b343))
(constraint (= (f #xddaa508e444736ea) #xddaa508e444736ea))
(constraint (= (f #x2647de621a5652b9) #x277a1d552b29054e))
(constraint (= (f #x47c75b8e06b0d5ba) #x47c75b8e06b0d5bb))
(constraint (= (f #x5556c65cce9398e0) #x5556c65cce9398e0))
(constraint (= (f #x77aa0bd00dd70b4a) #x77aa0bd00dd70b4a))
(constraint (= (f #x2de4dd44a0e33235) #x2f54042ec5ea4bc6))
(constraint (= (f #x4396a140218dda79) #x45b3564a229a494c))
(constraint (= (f #xab235bbbbe4b6cec) #xab235bbbbe4b6cec))
(constraint (= (f #x60e287eb5ea90ddd) #x63e99c2ab99e564b))
(constraint (= (f #x94e7e082a9b39775) #x998f1f86bf013430))
(constraint (= (f #x921ce0e3c77b4802) #x921ce0e3c77b4802))
(constraint (= (f #x28ee52a559e6736e) #x28ee52a559e6736e))
(constraint (= (f #x6c8e30b3ac9c3abe) #x6c8e30b3ac9c3abf))
(constraint (= (f #xab79907a779e1ce7) #xb0d55cfe4b5b0dce))
(constraint (= (f #x5deb6e100a77e359) #x60dac9808acba273))
(constraint (= (f #x692587e520c62c15) #x6c6eb42449cc5d75))
(constraint (= (f #x29b937b88c97209e) #x29b937b88c97209f))
(constraint (= (f #xc74ed579dc165ce0) #xc74ed579dc165ce0))
(constraint (= (f #x0e42bc341128b825) #x0eb4d215b1b1fde6))
(constraint (= (f #xbde69b94ca32aab8) #xbde69b94ca32aab9))
(constraint (= (f #x7a8463b44154ea0d) #x7e5886d1e35f915d))
(constraint (= (f #xc1e9105c40970d79) #xc7f858df229bc5e4))
(constraint (= (f #x3ed24b8b44c1ae59) #x40c8dde79ee7bbcb))
(constraint (= (f #x440588c91b0e763b) #x4625b50f63e6e9ec))
(constraint (= (f #x0a04673a1c557021) #x0a548a73ed381ba2))
(check-synth)
